$\forall$$T$:Type, ${\it eq}$:($T$$\rightarrow$$T$$\rightarrow\mathbb{B}$). IsEqFun($T$;${\it eq}$) $\Rightarrow$ (mk\_dset($T$, ${\it eq}$) $\in$ DSet)